
; Copyright (c) 2015 Microsoft Corporation
(set-option :auto-config true)

(declare-const v0 Int)
(declare-const v1 Int)

(assert 
(let ((?e2 0))
(let ((?e3 (* v1 ?e2)))
(let ((?e4 (* (~ ?e2) ?e3)))
(let ((?e5 (- ?e3 v1)))
(let ((?e6 (+ v1 v0)))
(let (($e7 (= ?e3 v0)))
(let (($e8 (<= ?e6 ?e5)))
(let (($e9 (< v1 ?e5)))
(let (($e10 (<= v1 ?e6)))
(let (($e11 (< v0 ?e4)))
(let ((?e12 (ite $e8 v0 ?e5)))
(let ((?e13 (ite $e9 ?e4 ?e3)))
(let ((?e14 (ite $e7 ?e6 ?e5)))
(let ((?e15 (ite $e10 ?e3 ?e5)))
(let ((?e16 (ite $e11 ?e13 v1)))
(let (($e17 (distinct ?e5 ?e14)))
(let (($e18 (>= ?e14 ?e4)))
(let (($e19 (< ?e15 ?e3)))
(let (($e20 (= ?e15 v0)))
(let (($e21 (>= v0 v0)))
(let (($e22 (distinct ?e16 ?e3)))
(let (($e23 (<= ?e13 ?e3)))
(let (($e24 (distinct ?e15 ?e13)))
(let (($e25 (<= ?e3 ?e6)))
(let (($e26 (<= ?e13 ?e15)))
(let (($e27 (= ?e5 v1)))
(let (($e28 (>= ?e5 ?e13)))
(let (($e29 (< ?e6 ?e12)))
(let (($e30 (not $e11)))
(let (($e31 (iff $e27 $e23)))
(let (($e32 (xor $e8 $e26)))
(let (($e33 (and $e7 $e29)))
(let (($e34 (iff $e25 $e25)))
(let (($e35 (implies $e21 $e17)))
(let (($e36 (implies $e34 $e24)))
(let (($e37 (if_then_else $e33 $e9 $e33)))
(let (($e38 (implies $e36 $e19)))
(let (($e39 (not $e18)))
(let (($e40 (if_then_else $e10 $e39 $e28)))
(let (($e41 (or $e38 $e31)))
(let (($e42 (xor $e37 $e22)))
(let (($e43 (if_then_else $e35 $e30 $e32)))
(let (($e44 (implies $e41 $e40)))
(let (($e45 (and $e44 $e44)))
(let (($e46 (xor $e43 $e45)))
(let (($e47 (if_then_else $e46 $e20 $e20)))
(let (($e48 (and $e42 $e47)))
$e48
)))))))))))))))))))))))))))))))))))))))))))))))
)

(check-sat)

